Nuprl Lemma : es-frame_wf
0,22
postcript
pdf
es
:ES,
i
:Id,
L
:Knd List,
x
:Id,
T
:Type. es-frame(
es
;
i
;
L
;
x
;
T
)
Prop
latex
Definitions
t
T
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
SQType(
T
)
,
Id
,
Prop
,
vartype(
i
;
x
)
,
x
when
e
,
(
x
after
e
)
,
ES
,
Knd
,
loc(
e
)
,
E
,
kind(
e
)
,
(
x
l
)
,
A
,
x
.
t
(
x
)
,
e
@
i
.
P
(
e
)
,
A
&
B
,
es-frame(
es
;
i
;
L
;
x
;
T
)
Lemmas
es-vartype
wf
,
alle-at
wf
,
not
wf
,
l
member
wf
,
es-kind
wf
,
es-E
wf
,
es-loc
wf
,
Knd
wf
,
event
system
wf
,
es-after
wf
,
es-when
wf
,
Id
wf
,
Id
sq
origin
es:ES, i:Id, L:Knd List, x:Id, T:Type. es-frame(es;i;L;x;T) 
Prop es:ES, i:Id, L:Knd List, x:Id, T:Type. es-frame(es;i;L;x;T) Prop T
Qx:A. B(x) l)
A
x. t(x)e@i. P(e)